Nuprl Lemma : filter2_wf
4,23
postcript
pdf
T
:Type,
L
:
T
List,
P
:(
||
L
||
). filter2(
P
;
L
)
T
List
latex
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
||
as
||
,
{
i
..
j
}
,
True
,
P
Q
,
False
,
A
,
A
B
,
,
T
,
S
T
,
if
b
t
else
f
fi
,
reduce2(
f
;
k
;
i
;
as
)
,
filter2(
P
;
L
)
Lemmas
reduce2
wf
,
ifthenelse
wf
,
squash
wf
,
true
wf
,
int
seg
wf
,
length
wf1
,
bool
wf
origin
T:Type, L:T List, P:(
||L||
). filter2(P;L) 
T List T:Type, L:T List, P:(||L||). filter2(P;L) T List Tx:A. B(x)
}
Q
A
B
T
T
t else f fi